Nuprl Lemma : causal_order_wf
4,23
postcript
pdf
T
:Type,
L
:
T
List,
P
,
Q
:(
||
L
||
Prop),
R
:(
||
L
||
||
L
||
Prop). causal_order(
L
;
R
;
P
;
Q
)
Prop
latex
Definitions
t
T
,
Prop
,
x
:
A
.
B
(
x
)
,
||
as
||
,
{
i
..
j
}
,
A
B
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
P
Q
,
causal_order(
L
;
R
;
P
;
Q
)
Lemmas
le
wf
,
int
seg
wf
,
length
wf1
origin
T:Type, L:T List, P, Q:(
||L||
Prop), R:(||L||||L||Prop). causal_order(L;R;P;Q) 
Prop T:Type, L:T List, P, Q:(||L||Prop), R:(||L||||L||Prop). causal_order(L;R;P;Q) Prop Tx:A. B(x)
}
B
x:A. B(x)
Q